\documentclass{llncs}

\usepackage{llncsdoc}
\usepackage{array}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{hhline}
\usepackage{epsfig}
\usepackage{listings}
\usepackage{subfigure}
\usepackage[table]{xcolor}
%%\usepackage{colortbl}
\usepackage{color}
\usepackage{epic,eepic}
\usepackage{url}
\usepackage{cite}
\usepackage{multirow}
\usepackage{graphicx}
\usepackage{wrapfig}

%%%%%%%%%%%%%%%%%%%%%% adding hyperlinks to help
%%%%%%%%%%%%%%%%%%%%%% paperless readers
\usepackage{color}
\usepackage{hyperref}
\definecolor{darkred}{rgb}{0.5,0,0}
\definecolor{darkgreen}{rgb}{0,0.5,0}
\definecolor{darkblue}{rgb}{0,0,0.5}
\hypersetup{ colorlinks,
linkcolor=darkblue,
filecolor=darkgreen,
urlcolor=darkred,
citecolor=darkblue }

\input{macros.tex}

\begin{document}

\frontmatter      % for the preliminaries
\mainmatter       % start of the contributions

\title{\tname{}: A novel approach to report data race warnings during
  state-space exploration}

\titlerunning{\tname{}: A novel approach to efficiently report accurate data
  race warnings}  % abbreviated title (for running head)

\author{Jo\~ao Paulo Oliveira\hspace{3ex} Marcelo d'Amorim\hspace{3ex}
  Fernando Castor}

\authorrunning{Jo\~ao Paulo Oliveira et al.} % abbreviated author list (for running head)
%
%%%% list of authors for the TOC (use if author list has to be modified)
\tocauthor{Jo\~ao Paulo Oliveira, Marcelo d'Amorim, and Fernando
  Castor Filho}
%
\institute{Federal University of Pernambuco\\
Informatics Center, Recife-PE, Brazil\\
\email{\{jpso,damorim,castor\}@cin.ufpe.br}
%% \texttt{http://users/\homedir iekeland/web/welcome.html}
%% \and
%% Universit\'{e} de Paris-Sud,
%% Laboratoire d'Analyse Num\'{e}rique, B\^{a}timent 425,\\
%% F-91405 Orsay Cedex, France
}

\maketitle              % typeset the title of the contribution

\begin{abstract}
Data races are a common kind of concurrency error found in
shared-memory programs that result in incorrect modification of
state.\Comment{ reachable from variables shared across different
  threads of the program.}  This paper presents \tname{}, a new
approach for data race detection that uses coverage information
obtained from the different schedules produced by a model checker to
\emph{predict} likely racy memory accesses.  \tname{} builds on the
observation that memory accesses are covered much sooner than the
actual race during state-space exploration.  We analyzed
\numSubjects{} subjects of various sources and sizes and implemented
our approach in the Java Pathfinder (JPF) model checker.  Results
indicate that \tname{} reports precise warnings of likely race very
soon compared to the time \jpf{} detects the race, that the warnings
it reports include few false alarms, and that the overhead on overall
exploration time is low, on average.
\end{abstract}

%% object and thread ids remain fixed across parts of the state-space
%% exploration and that



\input{intro}
\input{example}
\input{approach}
\input{eval}
\input{related}
\input{conclusions}

%
% ---- Bibliography ----
%
\bibliographystyle{plain}
\bibliography{testing}

\end{document}

% LocalWords:  d'Amorim Oliveira Alves Filho Pernambuco erma ao et al damorim
% LocalWords:  castor schedules jpso JPF
